#import "@preview/frame-it:1.1.2": *
#import "RoseL_Snippets.typ": *
#show: RoseLic

朴素集合论考虑用一些元素组成集合 ${a, b, c, dots}$, 或者将代入谓词使之成立的所有值组成集合 ${x | p(x)}$. 
将点视作元素, 线面体一律视作集合, 这样对用语的改造在几何学中获得了胜利. 

但在无穷集合, 集合的集合, 罗素悖论等问题面前, 朴素集合论捉襟见肘. 特别是罗素悖论, 它的真正解决还得等到冯·诺依曼提出基础公理, 强调成员关系的反自反性. 
冯·诺依曼也提出了很多规范集合理论的基本事实, 并且博内斯, 哥德尔等人对此进行过一些改进, 从而得到所谓冯·诺伊曼-博内斯-哥德尔集合理论, 也就是NBG公理集合论.

== 关于二元集的公理

// 我们预设一个#term[成员关系]作为基本概念. 
// 成员关系写成谓词就是 $in$, 

物以类聚. 谓词 "是" 常用来连结物件和它的类别, 比如 "的卢是马". 

#notation[成员关系 $in$ (element)][
成员关系是关于元素和类的谓词, 
通常说成 "元素属于类", 记作 $ a in C $
或者 "类包括元素" $C in.rev a$.
// 所有符合 $a in A$ 的二元组 (a,A) 组成成员关系类 E. 
#divide()
能属于某类的数学对象叫#term[元素], 习惯上用小写字母表示; 
$ exists C med (a in C) $
能包括某类的数学对象叫#term[类], 习惯上用大写字母表示. 
$ exists a med (a in C) $
既是元素又是类的叫做#term[集合],
是类而不是元素的叫做#term[真类],
是元素而不是类的叫做#term[真元素].
]
不特意为既不是元素又不是类的数学对象取名字, 但谓词一定是两不沾的, 比如 "$and in or$" 就是病态构成的式子, 事实上我们也不能说 $and in.not or$. 

#notation[描述法][
  给定一个谓词 $p$. 式 ${x | p(x)}$ 表达了由谓词 $p$ 所描述的类, 使得
  $ forall a med ( a in {x | p(x)} <--> p(a) ) $
]